Inference at * 1 1 1 
Iof proof for Lemma fseg extend:

.....subterm..... T:t1:n

1. T : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. L : T List
6. l2 = (L @ l1)
7. ||l1|| < ||l2||
8. l2[(||l2|| - (||l1||+1))] = v
9. (null(L))
10. L' : T List
11. L = (L' @ [last(L)])
  last(L) = v 

latex

 by (((Assert 0 < ||L||) 
THENL [(((DVar `L') 
CollapseTHEN (((All Reduce) 
CollapseTHEN (Auto'
C))))); Id]) 
CollapseTHEN (((((RevHypSubst (-5) 0) 
CollapseTHENA (Auto))) 
CollapseTHEN (
C((StrongHypSubst (-7) 0) 
CollapseTHENA (((Auto') 
CollapseTHEN (((HypSubst (-1) 0) 

CoCollapseTHEN (Auto')))))))))) 

latex

C1: 

C1: 12. 0 < ||L||
C1:   last(L) = (L @ l1)[(||L @ l1|| - (||l1||+1))]
C.

Definitions	a < b, #$n, ||as||, b, , [car / cdr], last(L), [], l[i], as @ bs, , t  T, , {x:A| B(x)} , x:A. B(x), s = t, type List, Type, A, False, P  Q, x:AB(x), Void, n - m, n+m, -n, A  B
Lemmas	select wf, nat wf, member wf, le wf